$\forall$$S$,$T$:Type, $P$,$Q$:($S$$\rightarrow\mathbb{P}$). ($S$ = $T$) $\Rightarrow$ ($\forall$$x$:$S$. \{$P$($x$) $\Rightarrow$ $Q$($x$)\}) $\Rightarrow$ \{($\exists$$x$:$S$. $P$($x$)) $\Rightarrow$ ($\exists$$y$:$T$. $Q$($y$))\}